/*******************************************************************************
 * Copyright (c) 2009 Kevin Bierhoff and others.
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 *     Kevin Bierhoff - initial API and implementation
 *******************************************************************************/
package com.googlecode.twelfdevtools.twelfast;

public class Sync extends AbstractTwelfAstVisitor<ITwelfAstNode> implements
		ITwelfAstVisitor<ITwelfAstNode> {
	
	/**
	 * Skips the given number of {@link Pi} terms in the given term
	 * and returns the remaining, inner term.
	 * @param t
	 * @param i
	 * @return the remaining, inner term.
	 */
	private static ITwelfTerm skipPis(ITwelfTerm t, int i) {
		if(i <= 0)
			return t;
		else
			return skipPis(((Pi) t).getTerm(), i-1);
	}

	/**
	 * Counts the number of {@link Pi} nodes on the onset of the given term.
	 * @param term
	 * @return the number of {@link Pi} nodes on the onset of the given term.
	 */
	private static int outerPiCount(ITwelfTerm term) {
		if(term instanceof Pi)
			return 1 + outerPiCount(((Pi) term).getTerm());
		else
			return 0;
	}

	private final ITwelfAstNode unboundTerm;

	public Sync(ITwelfAstNode unboundTerm) {
		this.unboundTerm = unboundTerm;
	}

	public ITwelfAstNode app(Application node) {
		Application other = (Application) unboundTerm;
		new Sync(other.getLhs()).doDispatch(node.getLhs());
		new Sync(other.getRhs()).doDispatch(node.getRhs());
		return node;
	}

	public ITwelfAstNode arrow(Arrow node) {
		Arrow other = (Arrow) unboundTerm;
		new Sync(other.getLhs()).doDispatch(node.getLhs());
		new Sync(other.getRhs()).doDispatch(node.getRhs());
		return node;
	}

	public ITwelfAstNode ascr(Ascription node) {
		Ascription other = (Ascription) unboundTerm;
		new Sync(other.getTerm()).doDispatch(node.getTerm());
		new Sync(other.getAscription()).doDispatch(node.getAscription());
		return node;
	}

	public ITwelfAstNode constDecl(ConstantDeclaration node) {
		ConstantDeclaration other = (ConstantDeclaration) unboundTerm;
		
		new Sync(other.getConst()).doDispatch(node.getConst());
		
		// skip inferred Pis in node.getTerm()
		ITwelfTerm t = node.getTerm();
		ITwelfTerm ut = other.getTerm();
		// TODO what about the value?
		int explicitPiCount = outerPiCount(t);
		int unboundPiCount = outerPiCount(ut);
		assert unboundPiCount <= explicitPiCount;
		t = skipPis(t, explicitPiCount - unboundPiCount);
		t.dispatch(new Sync(ut));

		// TODO what about the value?
		return node;
	}

	public ITwelfAstNode lambda(Lambda node) {
		if(unboundTerm instanceof Lambda) {
			Lambda other = (Lambda) unboundTerm;
			new Sync(other.getId()).doDispatch(node.getId());
			if(other.getIdTerm() != null)
				// can be omitted...
				new Sync(other.getIdTerm()).doDispatch(node.getIdTerm());
			new Sync(other.getTerm()).doDispatch(node.getTerm());
		}
		else {
			// Lambdas can be skipped...
			new Sync(unboundTerm).doDispatch(((Application) node.getTerm()).getLhs());
		}
		return node;
	}

	public ITwelfAstNode pi(Pi node) {
		Pi other = (Pi) unboundTerm;
		new Sync(other.getId()).doDispatch(node.getId());
		if(other.getIdTerm() != null)
			// can be omitted...
			new Sync(other.getIdTerm()).doDispatch(node.getIdTerm());
		new Sync(other.getTerm()).doDispatch(node.getTerm());
		return node;
	}

	public ITwelfAstNode type(Type node) {
		// "type" keyword has no binding
		return node;
	}

	public ITwelfAstNode id(Identifier node) {
		ITwelfBinding binding = node.getBinding();
		AbstractIdentifier unboundNode = (AbstractIdentifier) unboundTerm;
		unboundNode.setBinding(binding);
		if(binding instanceof VariableBinding) {
			// inject the source location if this identfier as the binding's location
			((VariableBinding) binding).setDefinitionRangeIfNotDefined(unboundNode);
		}
		return node;
	}

	public ITwelfAstNode wildcard(Wildcard node) {
		ITwelfBinding binding = node.getBinding();
		AbstractIdentifier unboundNode = (AbstractIdentifier) unboundTerm;
		unboundNode.setBinding(binding);
		if(binding instanceof VariableBinding) {
			// inject the source location if this identfier as the binding's location
			((VariableBinding) binding).setDefinitionRangeIfNotDefined(unboundNode);
		}
		return node;
	}

}
